Nuprl Lemma : eq_int_cases_test 13,42

A:Type, xy:AP:(A), ij:.
(P(if (i = j) then x else y fi ))  (P(if (i = j) then x else y fi )) 
latex


Upbool 1, bool 1
Definitionst  T, P  Q, , x:AB(x), x:AB(x), ff, tt, if b then t else f fi , Unit, , False, A, a  b  T ,
Lemmaseq int wf, ifthenelse wf, eq int eq false elim, eq int eq true elim, bool wf

origin